"""
This file illustrates how we can use code generation to implement
substitution in first-order abstract syntax.
"""


class Term:
    """ Base class for the language. """
    pass


class Lam(Term):
    def __init__(self, name, body):
        self.name = name
        self.body = body

    def __repr__(self):
        return "Lam(%r, %r)" % (self.name, self.body)

    def __str__(self, paren=False):
        s = "lam %s. %s" % (self.name, self.body.__str__(False))
        if paren:
            s = "(" + s + ")"
        return s

    def __call__(self, arg):
        # This is where the substitution takes place.
        # First we generate the code for an equivalent Python lambda function.
        code = "lambda %s: %s" % (self.name, self.body.hoas())
        # Then we evaluate the code to obtain the function.
        f = eval(code)
        # Finally we call the function on the argument.
        return f(arg)

    def evaluate(self):
        return Lam(self.name, self.body)
        # We could also evaluate inside the body
        return Lam(self.name, self.body.evaluate())

    def hoas(self):
        # We need to retrieve the bound variables back from Python variables.
        return "(lambda %s: Lam('%s', %s))(Var('%s'))" %(
            self.name, self.name, self.body.hoas(), self.name)


class Var(Term):
    def __init__(self, name):
        self.name = name

    def __repr__(self):
        return "Var(%r)" % self.name

    def __str__(self, paren=False):
        return self.name

    def evaluate(self):
        return Var(self.name)

    def hoas(self):
        # We transform this into a Python variable.
        return self.name


class App(Term):
    def __init__(self, left, right):
        self.left = left
        self.right = right

    def __repr__(self):
        return "App(%r, %r)" % (self.left, self.right)

    def __str__(self, paren=False):
        return "%s %s" % (self.left.__str__(True), self.right.__str__(True))

    def evaluate(self):
        return (self.left.evaluate())(self.right).evaluate()

    def hoas(self):
        return "App(%s, %s)" % (self.left.hoas(), self.right.hoas())
    

# Examples

I = Lam("x", Var("x"))
K = Lam("x", Lam ("y", Var("x")))
O = Lam("x", App(Var("x"), Var("x")))

print "I = ", I
print "K = ", K
print "O = ", O

print "Evaluation examples:"
print App(I, I), " => ", App(I, I).evaluate()
print App(K, K), " => ", App(K, K).evaluate()
# The following loops forever
#print App(O, O), " => ", App(O, O).evaluate()
